Nuprl Lemma : isect_prod_lemma
4,23
postcript
pdf
A
,
B
,
C
:Type.
A
B
A
C
(
A
B
C
)
latex
Definitions
S
T
,
T1
T2
,
x
:
A
.
B
(
x
)
,
t
T
,
P
&
Q
,
1of(
t
)
,
2of(
t
)
,
P
Q
,
Unit
,
,
x
.
t
(
x
)
Lemmas
pi2
wf
,
bool
wf
,
pi1
wf
,
isect2
decomp
,
isect2
wf
origin
A, B, C:Type. A
B 
AC 
(AB C) A, B, C:Type. AB AC (AB C) T T2x:A. B(x)
T
Q
x. t(x)